es:ES, T, T':Type, R:(TT'), P1, P2, Q1, Q2:(E), f:({e:E| P1(e)} {e:E| Q1(e)} ).
(e:E. P1(e)  (valtype(e) r T))
 (e:E. Q1(e)  (valtype(e) r T'))
 (e:E. P1(e)  P2(e))
 (e:E. Q1(e)  Q2(e))
 ((e.P1(e) e.f(e) e.Q1(e)) with R  (e.P2(e) e.f(e) e.Q2(e)) with R) 

latex

Definitions

P  Q, P  Q, P & Q, P  Q, x:A. B(x), t.1, E, f(a), x(s), valtype(e), t  T, x:A  B(x), b, ES, Type, x:AB(x), {x:A| B(x)} , , s = t, let x,y = A in B(x;y), (e.P(e) a.f(a) e'.Q(e')) with R, e c e', Bij(A;B;f), x. t(x), <a, b>, EqDecider(T), Unit, left + right, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), Top, s ~ t, {T}, SQType(T), (e < e'), x:A. B(x), Surj(A;B;f), Inj(A;B;f), A c B, e loc e' , (e <loc e'), P  Q, T, True

Lemmas

es-le-causle, es-causle-le, subtype rel set, causal-bijection wf, iff wf, es-valtype wf, es-E wf, event system wf